Nuprl Lemma : qminus-minus
11,40
postcript
pdf
x
:
. -(
x
) = (-
x
)
latex
Definitions
,
{
T
}
,
P
Q
,
SQType(
T
)
,
t
T
,
tt
,
if
b
then
t
else
f
fi
,
r
*
s
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
int
inc
rationals
origin
x:
. -(x) = (-x) 
x:. -(x) = (-x) 
Q Tx:A. B(x)
T